| 1: | a(lambda(x),y) | → lambda(a(x,p(1,a(y,t)))) | |
| 2: | a(p(x,y),z) | → p(a(x,z),a(y,z)) | |
| 3: | a(a(x,y),z) | → a(x,a(y,z)) | |
| 4: | a(id,x) | → x | |
| 5: | a(1,id) | → 1 | |
| 6: | a(t,id) | → t | |
| 7: | a(1,p(x,y)) | → x | |
| 8: | a(t,p(x,y)) | → y | |
| 9: | A(lambda(x),y) | → A(x,p(1,a(y,t))) | |
| 10: | A(lambda(x),y) | → A(y,t) | |
| 11: | A(p(x,y),z) | → A(x,z) | |
| 12: | A(p(x,y),z) | → A(y,z) | |
| 13: | A(a(x,y),z) | → A(x,a(y,z)) | |
| 14: | A(a(x,y),z) | → A(y,z) | |